Возможно ли научить компьютер доказывать теоремы? Оказывается, существуют специальные системы, такие как Z3, которые не только автоматически доказывают теоремы, но также тестируют программное обеспечение, анализируют и проверяют его.

На научно-техническом семинаре Николай Бьернер расскажет про открытую систему автоматического доказательства теорем Microsoft Z3 и ее применении. После семинара у слушателей будет возможность пообщаться с докладчиком в неформальной обстановке.

Семинар пройдет на английском языке. Начало в 19.00. Регистрация обязательна (http://events.yandex.ru/events/science-seminars/Bjorner-oct-2012/).

_____________________________________________________________________________

This talk describes the Satisfiability Modulo Theories (SMT) solver, Z3, from Microsoft Research. Z3 is a state-of-the art theorem prover that integrates specialized solvers for domains that are of relevance for program analysis, testing and verification. Z3 is a compelling integral component of such tools because these tools rely on reasoning about program states and transformations between states in ways that are slightly disguised as SMT problems.
We describe uses of Z3, including the Windows 7 static driver verifier, the SAGE white-box fuzzer for finding security vulnerabilities, a cloud service security policy checker, the Pex test-case generation tool, a verifying C compiler and JavaScript malware detection, among others. We also give an overview of recent advances in modern high-performance theorem provers. This includes algorithms and indexing data-structures for efficiently combining solvers, efficient ground decision procedures, and scalable reasoning with quantifiers.

Яндекс

ya-events@yandex.ru